#include <iostream>
#include <fstream>
#include <sstream>
#include <string>
#include <vector>
#include <memory>
#include <algorithm>
#include "termat.h"
#include "tervec.h"

// ParseCNF parses a DIMACS CNF file into a TerMat
std::shared_ptr<TerMat> ParseCNF(const std::string& filename, int& vars, bool& ok) {
    std::ifstream file(filename);
    if (!file) {
        std::cerr << "Error opening file: " << filename << std::endl;
        ok = false;
        return nullptr;
    }
    std::string line;
    std::shared_ptr<TerMat> mat;
    while (std::getline(file, line)) {
        line.erase(0, line.find_first_not_of(" \t\n\r"));
        if (line.empty() || line[0] == 'c' || line[0] == '%') continue;
        if (line.substr(0, 5) == "p cnf") {
            std::istringstream iss(line);
            std::string p, cnf;
            iss >> p >> cnf >> vars;
            int clauses;
            iss >> clauses;
            mat = std::make_shared<TerMat>(vars);
            continue;
        }
        std::istringstream iss(line);
        std::vector<int> terms;
        int lit;
        while (iss >> lit) {
            terms.push_back(lit);
        }
        if (!mat) {
            std::cerr << "CNF header (p cnf ...) must appear before clauses." << std::endl;
            ok = false;
            return nullptr;
        }
        if (terms.empty()) continue;
        auto vec = std::make_shared<TerVec>(0, 0, vars);
        bool hasLiterals = false;
        for (int literal : terms) {
            if (literal == 0) {
                if (!hasLiterals) {
                    ok = false;
                    return nullptr;
                }
                mat->add(vec);
                break;
            } else {
                hasLiterals = true;
                vec->set({literal});
            }
        }
    }
    ok = true;
    return mat;
}

int main(int argc, char* argv[]) {
    if (argc < 2 || argc > 3) {
        std::cout << "Usage: penponism <cnf_file> [--verbose|-v]" << std::endl;
        return 1;
    }
    std::string filename = argv[1];
    int vars = 0;
    bool ok = false;
    auto mat = ParseCNF(filename, vars, ok);
    if (!ok || !mat) {
        std::cerr << "Failed to parse CNF file" << std::endl;
        return 1;
    }

    bool verbose = false;
    if (argc == 3 && (std::string(argv[2]) == "--verbose" || std::string(argv[2]) == "-v")) {
        verbose = true;
    }

    mat->sort();
    std::cout << "Parsed CNF file with " << vars << " variables and " << mat->len() << " clauses" << std::endl;
    std::cout << "\nOriginal clauses:" << std::endl;
    mat->print();

    // 1. Disjoint union by sequentially adding clauses (DiffVerbose)
    std::cout << "\nDisjoint union (DiffVerbose):" << std::endl;
    auto disjointResult = mat->diffVerbose(verbose, true);
    std::cout << "Disjoint union result has " << disjointResult->len() << " clauses" << std::endl;
    // Optionally print the result
    // disjointResult->print();

    // 2. Pairwise intersections (OuterComm)
    // std::cout << "\nPairwise intersections (OuterComm):" << std::endl;
    // auto outerCommResult = mat->outerComm();
    // outerCommResult->sort();
    // outerCommResult->dedup();
    // outerCommResult->reduce();
    // std::cout << "Pairwise intersection result has " << outerCommResult->len() << " clauses" << std::endl;
    // // Optionally print the result
    // // outerCommResult->print();

    return 0;
} 